型理論 インデックス
型理論
依存型理論(Martin-Löf型理論)
型システム
型理論、依存型理論を学習する
判断
項
Calculus of Constructions
Calculus of Inductive Constructions(CIC)
型理論と他の領域で対応するものある系の話
型と集合
Sets as Types, Types as Sets
型と論理
カリー＝ハワード対応
Propositions as Types
ハイパードクトリン
ホモトピー型理論から様相論理へのルートを考える
Modal Homotopy Type Theoryがホモトピー型理論と様相論理をあわせたもの
型と圏論
型理論と論理と圏論
カリー／ハワード／ランベック対応
ハイパードクトリン
ホモトピー型理論と論理・集合・圏論など？の関係
型をホモトピー的に扱う
Homotopy Type Theory(HoTT)
Cubical Type Theory
Observational Type Theory
Modal Homotopy Type Theory
○○ as ○○
Sets as Types, Types as Sets
Propositions as Types
パラドックス関連
可述的
非可述的
ラッセルのパラドックス
ジラールのパラドックス
Hurkensのパラドックス
文献
型理論の文献
関連
形式手法
#インデックスページ #ハブページ